<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue2733-2</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\begin{document}

\begin{AgdaAlign}
</a><a id="81" class="Markup">\begin{code}</a>
<a id="94" class="Keyword">module</a> <a id="101" href="Issue2733-2.html" class="Module">Issue2733-2</a> <a id="113" class="Keyword">where</a>
<a id="119" class="Markup">\end{code}</a><a id="129" class="Background">

Indentation should be inserted before \AgdaKeyword{postulate}, but not
before the last occurrence of \AgdaPrimitiveType{Set}, which should be
aligned with the penultimate occurrence of \AgdaPrimitiveType{Set}:
</a><a id="341" class="Markup">\begin{code}</a>
  <a id="356" class="Keyword">postulate</a>
    <a id="A"></a><a id="370" href="Issue2733-2.html#370" class="Postulate">A</a>  <a id="373" class="Symbol">:</a> <a id="375" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    <a id="B"></a><a id="383" href="Issue2733-2.html#383" class="Postulate">B</a>  <a id="386" class="Symbol">:</a> <a id="388" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="392" class="Symbol">→</a>
         <a id="403" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="407" class="Markup">\end{code}</a><a id="417" class="Background">
\end{AgdaAlign}

\end{document}
</a></pre></body></html>